Date: Fri, 04 May 2001 From: "John F. Sowa" I agree that more examples would be helpful. Following are your two examples translated to CGs. I'm sending this note to CG and SUO lists because there may be other people who might find it useful. > In your material on CG's that I have seen, I have not found how to > express simple rules of deduction. If you could provide an example or two, > and say something about how a proof engine would use them, I would find > this very helpful. For the theoretical foundations of CGs, I use Peirce's rules of inference. For P's own statement of the rules with my commentary and explanation, see the annotated version of his Manuscript 514: http://www.bestweb.net/~sowa/peirce/ms514.htm These rules are general enough that all other proof procedures for FOL can be proved as derived rules of inference, including resolution and natural deduction. For any proof that uses predicate calculus notation, there is a formally equivalent proof that uses CG notation and vice versa. Peirce's rules usually give the shortest proofs (even when adapted to predicate calculus notation). Following are your examples translated to CG notation. For the proof procedure, I'll use a version of P's rules adapted to CG notation. > Rule: > If x is a passenger on bus y > And bus y is going to city z > then x is going to city z When CG's are generated from natural language sentences, linguistic relations, such as Agnt (for agent) and Dest (for destination) are commonly used. But it is also possible to represent verbs as relations, as I illustrate in the CG tutorial: http://www.bestweb.net/~sowa/cg/tut.htm To reduce the total number of nodes in the CGs and to simplify the discussion, I'll use a dyadic relation named (GoR2): [If: [Passenger: *x]->(On)->[Bus: *y] [Bus: *y]->(GoR2)->[City: *z] [Then: [?x]->(GoR2)->[?z] ] ] The type labels "If" and "Then" are syntactic sugar for contexts with a relation (Neg) or ~ for negation attached to them. Note that the "Then" context is nested inside the "If" context. That nesting is necessary to ensure that any variable (coreference label) in the "Then" context is within the scope of its defining node in the "If" context. In the linear notation, contexts are marked with square brackets, and in the display form, they are represented by boxes. (Peirce used ovals.) > Facts: > John is on bus 19 > bus 19 is going to Boston [Person: "John"]->(On)->[Bus: "19"] [Bus: "19"]->(GoR2)->[City: "Boston"] > Deduction > John is going to city Boston Peirce's rules of inference can be used in a way that is very similar to resolution (in fact, resolution is a derived rule of inference that can be proved from P's rules). 1. By deiteration, any graph in a nested context that is the same (or can be made the same by graph unification) can be erased after doing the unification (which in CGs corresponds to a copy followed by a maximal join). First do the unification with the two facts: [If: [Passenger: "John"]->(On)->[Bus: "19"] [Bus: "19"]->(GoR2)->[City: "Boston"] [Then: [Passenger: "John"]->(GoR2)->[City: "Boston"] ] ] Note: The type labels "Passenger" and "City" can be omitted if they are already present on an outer coreferent concept, since they state redundant information. For clarity, they may be copied into the inner concept, if desired. (But there is no requirement to do so.) Now erase the two graphs in the "If" context: [If: [Then: [Passenger: "John"]->(GoR2)->[City: "Boston"] ] ] Since "If" and "Then" are synonyms for negations, they can both be erased by the rule of double negation: [Passenger: "John"]->(GoR2)->[City: "Boston"] > Next challenge would be to handle negation. e.g.: > Rule: > If x is going to city y > And z is not equal to y > then x is not going to city z Handling negation is simple: You can just put brackets around the CG with the relation (Neg) or its abbreviation by ~ in front. [If: [*x]->(GoR2)->[City: *y] ~[ [?z]- - -[?y] ] [Then: ~[ [?x]->(GoR2)->[City: ?z] ] ] ] The dotted line is a coreference link. It expresses equality of the referents of the two concept nodes. The ~ represents negation. However, there are more serious questions about names and equality. In any system of logic, you have to make some kind of assumption. For example, is "New York" the same or equal to "New York City" or "New York State"? Is "NYC" the same as "New York City"? Is "Cicero" the same as "Tully"? Is "Boston" the same as "Washington"? To avoid getting into those issues, I will add the following fact: ~[ [City: "Boston"]- - -[City: "Washington"] ] This says it is false that the city named "Boston" is equal to (coreferent with) the city named "Washington" > Facts: > John is going to city Boston [Person: "John"]->(GoR2)->[City: "Boston"] > Deduction > John is not going to Washington As before, unify the two facts with the two CGs in the "If" context: [If: [Person: "John"]->(GoR2)->[City: "Boston"] ~[ [City: "Washington"]- - -[City: "Boston"] ] [Then: ~[ [Person: "John"]->(GoR2)->[City: "Washington"] ] ] ] As before, the CGs in the "If" context can be erased by the rule of deiteration, and the "If" and "Then" brackets can be erased by the rule of double negation. The result is ~[ [Person: "John"]->(GoR2)->[City: "Washington"] ] This says it is false that the person named "John" is going to the city named "Washington". The above examples are stated in the informal linear notation for CGs. The draft CG standard uses CGIF (CG Interchange Form) as the only normative notation. Following are the above graphs translated to CGIF and KIF. John Sowa ________________________________________________________________________ CGIF for example 1: [If: (On [Passenger: *x] [Bus: *y]) (GoR2 [Bus: *y] [City: *z]) [Then: (GoR2 ?x ?z) ] ] (On [Person: "John"] [Bus: "19"]) (GoR2 [Bus: "19"] [City: "Boston"]) (GoR2 [Passenger: "John"] [City: "Boston"]) KIF: (=> (and (Passenger ?x) (Bus ?y) (On ?x ?y) (City ?z) (GoR2 ?y ?z) ) (GoR2 ?x ?z) ) (and (Person John) (Bus Bus19) (On John Bus19) (and (Bus Bus19) (City Boston) (GoR2 Bus19) (City Boston)) (and (Passenger John) (City Boston) (GoR2 John Boston)) Note: Some coventions are needed for translating names in English to CGs and KIF. In CGIF, names are quoted, and they are not considered unique identifiers unless some additional assumption is stated. In KIF, constants are represented by identifiers, which are not quoted, and it is not clear whether they should be considered identical to the names that are used in the English sentence. In the CG standard, I define [Person: "John"] to be an abbreviation for (Name [Person] [Word: "John"]), which says that there exists a person whose name is the word "John". This makes a clear separation between the names used in English and the identifiers in the formalism. That expanded form would map to the following KIF expression: (exists (?x) (and (Person ?x) (Word "John") (Name ?x "John"))) _______________________________________________________________________ For example 2, the KIF and CGIF statements are similar to the ones above. The only new feature is the negation and the equality: The dotted line is represented by placing a defining coreference label on the first concept, such as *x and a bound label ?x on the second. Following is the informal linear notation: ~[ [City: "Boston"]- - -[City: "Washington"] ] which can be translated to the following form in CGIF: ~[ [City: "Boston" *x] [City: "Washington" ?x] ] In KIF, the coreference label *x or ?x would map to a variable ?x. Or you could use Boston and Washington as the names of KIF constants: (not (and (City Boston) (City Washington) (= Boston Washington)))